A, T:Type, L:T List, k:A, i:, f:(T{i..(i+||L||)}AA).
reduce2(f;k;i;L) = reduce2(x,i,l. f(x,i-1,l);k;i+1;L)  A 

latex

Definitions	, t  T, x:A. B(x), ||as||, {i..j}, ij, AB, P & Q, i  j < k, S  T, P  Q, False, A, S  T
Lemmas	le wf, non neg length, int seg wf, length wf1, nat wf